Nuprl Lemma : non-neg-qmul
11,40
postcript
pdf
a
,
b
:
. 0
a
0
b
0
a
*
b
latex
Definitions
True
,
T
,
P
Q
,
P
Q
,
P
&
Q
,
{
T
}
,
P
Q
,
P
Q
,
x
:
A
.
B
(
x
)
,
,
t
T
,
S
T
Lemmas
qmul
comm
qrng
,
true
wf
,
squash
wf
,
member
wf
,
qmul
zero
qrng
,
qmul-positive
,
qless
wf
,
qmul
wf
,
int
inc
rationals
,
qle
wf
,
rationals
wf
origin
a, b:
. 0 
a 
0 b 0 a * b a, b:. 0 a 0 b 0 a * b 
T
Q Q
Q Qx:A. B(x)
T
T